coq 8.19.0; math-comp 1.19.0 - #162403
Conversation
github-actions
Bot
added
the
ocaml
|
You can fix the CI failure by bumping the revision in the math-comp formula (see #135135 for an example). |
6dbc6b6 to
c50ef69
Compare
|
Looks like an actual incompatibility with the version of math-comp in the formula and coq 8.19: Appears to be an (undocumented) side effect of rocq-prover/rocq#17576 and addressed by math-comp/math-comp#1115, which was included in math-comp 1.19.0. |
|
Putting both coq and math-comp in the same PR seems like the least objectionable way to deal with this. If they're in separate PRs and math-comp lands first, then the bottle gets built with the old coq, and so the coq PR would need to bump math-comp's revision immediately. On the other hand, if the coq PR lands first, then there would be a gap between then and when the math-comp PR lands when math-comp's bottles wouldn't work. If they're in the same PR, they land simultaneously, and there is no interval when a |
|
馃 An automated task has requested bottles to be published to this PR. |
github-actions
Bot
added
the
CI-published-bottle-commits
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?s=60&v=4){kind=small}
5 participants
HOMEBREW_NO_INSTALL_FROM_API=1 brew install --build-from-source <formula>, where<formula>is the name of the formula you're submitting?brew test <formula>, where<formula>is the name of the formula you're submitting?brew audit --strict <formula>(after doingHOMEBREW_NO_INSTALL_FROM_API=1 brew install --build-from-source <formula>)? If this is a new formula, does it passbrew audit --new <formula>?